COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002
C00003 ENDMK
C⊗;



   samefringe[x, y] ← 
     [¬at x ∧ ¬at y ∧ same[a x, a y, d x, d y]] ∨ x eq y



   same[x, y, u, v] ← 
     [¬at x ∧ ¬at y ∧ same[a x, a y, d x . u, d y . v]]
     ∨ [¬at y ∧ same[x, a y, u, d y . v]]
     ∨ [¬at x ∧ same[a x, y, d x . u, v]]
     ∨ [x eq y ∧ samefringe[u, v]]